FDL - Nuprl Lemma : prod-deq-aux

Nuprl Lemma : prod-deq-aux_wf

0,22

A, B:Type{i}, a:EqDecider(A), b:EqDecider(B).
prod-deq-aux{v:l, i:l}(A; B; a; b)

(

p, q:(A

B). p = q

proddeq(a;b)(p,q))

Definitions t T, x:A. B(x), EqDecider(T), proddeq(a;b), b, Prop, P Q, proddeq-property, prod-deq-aux{v:l,i:l}(A;B;a;b)

Lemmas proddeq-property, iff wf, assert wf, proddeq wf, deq wf

Definitions	t T, x:A. B(x), EqDecider(T), proddeq(a;b), b, Prop, P Q, proddeq-property, prod-deq-aux{v:l,i:l}(A;B;a;b)
Lemmas	proddeq-property, iff wf, assert wf, proddeq wf, deq wf